chore: put asymmetric patterns commands on separate lines#2356
Merged
Alizter merged 5 commits intoHoTT:masterfrom Apr 24, 2026
Merged
chore: put asymmetric patterns commands on separate lines#2356Alizter merged 5 commits intoHoTT:masterfrom
Alizter merged 5 commits intoHoTT:masterfrom
Conversation
Split the combined `Set Asymmetric Patterns.
#[warning="-unknown-option"] Set Asymmetric Patterns No Implicits.` line
into separate lines across all 127 affected files:
Set Asymmetric Patterns.
#[warning="-unknown-option"]
Set Asymmetric Patterns No Implicits.
Also add a comment in `theories/Basics/Settings.v` noting that the
warning clause can be removed once our minimum Rocq version is 9.3.
Signed-off-by: Ali Caglayan <alizter@gmail.com>
Signed-off-by: Ali Caglayan <alizter@gmail.com>
jdchristensen
approved these changes
Apr 24, 2026
Collaborator
jdchristensen
left a comment
jdchristensen
left a comment
There was a problem hiding this comment.
I quickly reviewed it and it looks better. I noticed a few places where no blank lines were left between the last settings line and the next line. I fixed two in the github GUI, but then found more and stopped trying. (Github wouldn't let me create suggested edits for these.) So this looks fine, or the blank lines in a few more places could be restored if you feel like it.
My edit to the first comment assumes that this is now the only place with this warning clause, but I didn't check that.
Co-authored-by: Dan Christensen <jdc+github@uwo.ca>
Collaborator
Author
|
Yes, this should be the only place now. The others turned out to be unnecessary like you said. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Cleanup what was started in #2355 and remove redundant settings from Categories/.